interface{-}val(${\it es}$;$X$;$e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$X$locknd{-}deq()($<$es{-}loc(${\it es}$; $e$), es{-}kind(${\it es}$; $e$)$>$)(es{-}state{-}when(${\it es}$;$e$),es{-}val(${\it es}$; $e$))